COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	davis.rev[f81,jmc]	Review of Martin Davis NSF proposal
C00005 ENDMK
C⊗;
davis.rev[f81,jmc]	Review of Martin Davis NSF proposal

	All three fields mentioned in this proposal can benefit
from the attention of a logician of Martin Davis's ability.
His ability to bring students into these fields and supervise
them is also important.

	I
am most familiar with the scientific situation in non-monotonic
reasoning, because it is so new.  It is now clear that almost
all human common sense reasoning involves some monotonicity, i.e. some
processs of assuming that the relevant facts are those that
are being taken into account and that the entities whose existence
can be deduced from these facts are the relevant entities.  It is
also clear that intelligent computer programs must also reason
non-monotonically as well as deductively.  It presents many problems,
both practically and theoretically that require work in mathematical
logic.
At present, Davis is the only person
with a record of accomplishment in mathematical logic who is
doing anything in the field.

	The field of characterizing adequate sets of test cases for
programs is somewhat better developed, but again a logicians point
of view is important.

	Martin Davis is, as he says, one of the originators of
computer theorem proving.  No doubt he has further contributions
to make.

	I am somewhat surprised at the modesty of the budget
proposed.  The proposal should certainly be fully supported.